Section: New Results

Mobile Ad-Hoc Networks

Participants : Mathilde Arnaud, Morten Dahl, Stéphanie Delaune, Graham Steel.

Mobile ad hoc networks consist of mobile wireless devices which autonomously organize their communication infrastructure: each node provides the function of a router and relays packets on paths to other nodes. Finding these paths in an a priori unknown and constantly changing network topology is a crucial functionality of any ad hoc network. Specific protocols, called routing protocols, are designed to ensure this functionality known as route discovery. Secure routing protocols use cryptographic mechanisms in order to prevent a malicious node from compromising the discovered route and they often perform some recursive tests on received messages.

Mathilde Arnaud, Véronique Cortier and Stéphanie Delaune provide NPTIME decision procedures for protocols with recursive tests and for a bounded number of sessions [26] . They also revisit constraint system solving, providing a complete symbolic representation of the attacker knowledge.

In the context of vehicular ad-hoc networks, to improve road safety, a vehicle-to-vehicle communication platform is currently being developed by consortia of car manufacturers and legislators.

In [35] , Morten Dahl, Stéphanie Delaune and Graham Steel propose a framework for formal analysis of privacy in location based services such as anonymous electronic toll collection. They give a formal definition of privacy, and apply it to the VPriv scheme for vehicular services. They analyse the resulting model using the ProVerif tool, concluding that the privacy property holds only if certain conditions are met by the implementation. Their analysis includes some novel features such as the formal modelling of privacy for a protocol that relies on interactive zero-knowledge proofs of knowledge and list permutations.